Inducing syntactic cut-elimination for indexed nested sequents

摘要

The key to the proof-theoretical study of a logic is a cutfree proofcalculus. Unfortunately there are many logics of interest lacking suitableproof calculi. The proof formalism of nested sequents was recently generalisedto indexed nested sequents in order to yield cutfree proof calculi forextensions of the modal logic K by Geach (Lemmon-Scott) axioms. The proofs ofcompleteness and cut-elimination therein were semantical and intricate. Here weidentify a subclass of the labelled sequent formalism and show that itcorresponds to the indexed nested sequent formalism. This correspondence isthen exploited to induce syntactic proofs for indexed nested sequents using theelegant existing proofs in the labelled sequent formalism. A larger goal ofthis work is to demonstrate how specialising existing proof-theoreticaltransformations (adapting these as required to remain within the subclass) isan alternative means of argument which can alleviate the need for independentproofs from `scratch' in each formalism. Moreover, such coercion can be used toinduce new cutfree calculi. We demonstrate by presenting the first indexednested sequent calculi for intermediate logics. Finally, we introduce a notionof duplicate subgraph using certain graph automorphisms---generalising thenotion of contraction for labelled sequents whose underlying structure is moregeneral than trees---yielding a normal form for derivations. We envisage thatsuch notions might be employed in order to prove decidability of a logic usingits restricted labelled calculus.